Nuprl Definition : es-triggers-params-consistent 11,40
es-triggers-params-consistent(es;A;i;ds;conds)
== (k:Knd. (k  dom(conds))  (hasloc(k;i)))
== & (e:E. (loc(e) = i)  (kind(e)  dom(conds))  (valtype(e) r (conds(kind(e)).1)))
== & ((k:Knd. (k  dom(conds)))  (state@i r State(ds))) 
latex

clarification:

es-triggers-params-consistent(es;A;i;ds;conds)
== (k:Knd. (fpf-dom(KindDeq; k; conds))  (hasloc(k;i)))
== & (e:es-E(es).
== & ((es-loc(es; e) = i  Id)
== & ( (fpf-dom(KindDeq; es-kind(es; e); conds))
== & ( (es-valtype(es; e) r (condsKindDeq(es-kind(es; e)).1)))
== & ((k:Knd. (fpf-dom(KindDeq; k; conds)))  (es-state(es;i) r State(ds))) 
latex

Definitionshasloc(k;i), P & Q, x:A. B(x), E, s = t, Id, loc(e), valtype(e), t.1, f(x), kind(e), P  Q, x:A. B(x), Knd, b, x  dom(f), KindDeq, state@i, State(ds)
FDL editor aliaseses-triggers-params-consistent

origin